/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.semantic;

import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.Map;
import java.util.Set;

import alloy.ast.ASTDepthFirstVisitor;
import alloy.ast.CardinalityExpr;
import alloy.ast.Command;
import alloy.ast.Decl;
import alloy.ast.ElemIntFormula;
import alloy.ast.FindCommand;
import alloy.ast.Formula;
import alloy.ast.FormulaSeq;
import alloy.ast.Formulas;
import alloy.ast.IntCompOp;
import alloy.ast.LeafId;
import alloy.ast.LiteralIntExpr;
import alloy.ast.Module;
import alloy.ast.ModuleInfo;
import alloy.ast.Multiplicity;
import alloy.ast.MultiplicityExpr;
import alloy.ast.Node;
import alloy.ast.QualifiedName;
import alloy.ast.Scope;
import alloy.ast.SetMultExpr;
import alloy.ast.SigExpr;
import alloy.ast.Signature;
import alloy.ast.Specification;
import alloy.ast.TypeScope;
import alloy.ast.Variable;
import alloy.subscope.ScopedSigsInfo;
import alloy.subscope.ScopedSigsInfoImpl;
import alloy.type.RelationType;
import alloy.type.SigType;
import alloy.type.UnionType;
import alloy.util.Dbg;
import alloy.util.Msg;


/**

 * A visitor which checks commands for semantic correctness.  Checks include making
 * sure the names referenced and the scope specifications are valid.  Also builds
 * a table representation of the scope specification of each command. 
 *
 * <p>Also, generates information about product sigs for each command, stored in
 * {@link alloy.ast.Command#productSigIdToRels}.
 */

public class CommandVisitor extends ASTDepthFirstVisitor implements alloy.util.AlloyConstants {

    /** the module scope for the current module */
    private ModuleInfo _moduleInfo;

    /** information about scoped sigs for the current model */
    private ScopedSigsInfo _scopedSigsInfo;
    
    public void visit(Specification spec_) {
	visit(spec_.getFocus());
    }

    public void visit(Module module_) {
        // set the current module scope
        _moduleInfo = module_.getModuleInfo();
	// set the current scoped sigs info
	_scopedSigsInfo = new ScopedSigsInfoImpl(SigType.getStringToType());
        // visit children
        visit((Node)module_);
	
    }

    /** visit a find command for semantic correctness **/
    public void visit(FindCommand findCommand_) {
	//System.out.println("Checking COMMAND " + findCommand_.nodeString());
	// now, ensure scope is correct and create scope table
	_checkScope(findCommand_);

	if (Dbg.userError)
	    return;

	// add implicit scope constraints to the formula
	_generateScopeConstraints(findCommand_, 
				  ((FormulaSeq) findCommand_.formula).getFormulas());

	// set the command's stringToType to contain only scoped types
	_generateScopedStringToType(findCommand_);

	//System.out.println("FIND COMMAND " + findCommand_.formula.pp());
	
    }

    /**
     * Sets command_'s stringToType to contain only scoped types (those found 
     * in the command's leafId2Scope
     **/
    private void _generateScopedStringToType(Command command_) {
	////System.out.println("in _generateScopedStringToType");
	command_.stringToType = new HashMap();
	//System.out.println("in _generateScopedStringToType: " + command_.nodeString());
	for (Iterator idIter = command_.leafId2Scope.keySet().iterator(); idIter.hasNext();) {
	    LeafId id = (LeafId) idIter.next();
	    String name = _scopedSigsInfo.getScopedSigName(id);
	    if (SigType.getSigTypeForString(name) == null) {
		Dbg.check(SigType.getSigTypeForString(name) != null, 
			  "no SigType for " + name);
	    }
	    //System.out.println(name + " : " + command_.leafId2Scope.get(id));
 
	    command_.stringToType.put(name, SigType.getSigTypeForString(name));
	}

	
    }

    /**
     * @return true if the signature identified by id_ is a transitive subtype of a 
     * signature identified by a LeafId in exactlyScopedSigs_;
     * otherwise returns false
     **/
    private boolean _childOfExactlyScopedSig(LeafId id_, Set exactlyScopedSigs_) {
	if (exactlyScopedSigs_.contains(id_))
	    return true;
	LeafId parentId = _scopedSigsInfo.parentSigId(id_);
	return (parentId == null ? 
		false : 
		_childOfExactlyScopedSig(parentId, exactlyScopedSigs_));
    }
    
    /**
     * Generates set cardinality constraints from command_.getScope() 
     * and adds them to formulas_.  
     * For example, the scope of the command 'run show for exactly 3 A' will add the 
     * constraint '#A = 3' to formulas_.
     **/
    private void _generateScopeConstraints(Command command_, Formulas formulas_) {
	// Set[LeafId].  This set contains the ids of signatures with exact scope
	Set handled = new HashSet();
	// iterate over all the scoped types, and add the set cardinality constraint
	// for all exactly set scopes and their children (i.e. saying "run show for 3
	// but exactly 4 A, 2 A1" will treat "2 A1" as "exactly 2 A1" if A1 is a 
	// subtype of A
	for (Iterator scopeIter = command_.getScope().getTypeScopes().getTypeScopeIter(); 
	     scopeIter.hasNext();) {
	    TypeScope typeScope = (TypeScope)scopeIter.next();
	    
	    SigExpr sigExpr = typeScope.getSigExpr();
	    // skip spec of "int"
	    if (sigExpr.nodeString().equals("int")) { 
		continue; 
	    }
            
	    Signature sig = _moduleInfo.getSignature(sigExpr.getSig(), null);
	    
	    if (typeScope.isExact() || _childOfExactlyScopedSig(sig.getLeafId(), handled)) {
		Formula cardFormula = 
		    new ElemIntFormula(new CardinalityExpr(sig.toSigExpr()), 
				       IntCompOp.INT_EQUALS,
				       new LiteralIntExpr(typeScope.getBound()));
		// we set the LeafIds on the newly created formula
		cardFormula.applyVisitor(command_.sliv);
		formulas_.addFormula(cardFormula);
		handled.add(sig.getLeafId());
	    }
	    
	}

    }

    /** check the scope for a command and built a table 
	representation of the scope, mapping each type
        to its scope */
    private void _checkScope(Command command_) {
        
        // construct a mapping of the type Strings to the scope of the type,
        // checking for semantic errors in the process
        command_.leafId2Scope = new HashMap();
        command_.productSigIdsToRels = new HashMap();
	
	Scope scope = command_.getScope();
	// first, add the specified scopes to the mapping, checking for an error
        if (!_addTypeScopesToMapping(scope, command_.leafId2Scope)) return;
     
	Set explicitlyScopedSigs = new HashSet(command_.leafId2Scope.keySet());

        // now, iterate through all types and give all unscoped types
	// an implicit scope, if possible
        int defaultScope = scope.getDefaultScope();
        for (Iterator typeIter = SigType.getSigTypeStrings().iterator();
	     typeIter.hasNext();) {
            String curType = (String)typeIter.next();
            if (_isProductSig(curType)) { 
		continue; // handle in separate pass
            }
	    if (_scopeType(curType, command_.leafId2Scope, defaultScope) < 0) {
		// unscoped top-level type
		if (_isTopLevel(_sigLeafId(curType))) {
		    Dbg.user(new Msg("no scope specified for top-level type " 
				     + curType + " in command", scope));
		}
		// unscoped type with explicitly scoped subtype -- generate error
		// for all but univ
		if (_sigLeafId(curType) != _moduleInfo.getUniv().getLeafId() &&
		    _hasScopedSubtype(_sigLeafId(curType), explicitlyScopedSigs)) {
		    Dbg.user(new Msg(curType 
				     + " must be assigned a scope since " +
				     "it has a scoped subtype.", 
				     scope));
		} 
	    }
	}
	
	// the above algorithm will not assign a scope to univ if there 
	// are no signatures except univ in the model (this is because the algorithm
	// only ensures that "top-level" signatures are scoped -- top-level signatures
	// are defined to be direct descendents of univ).  
	// In this case, command_.leafId2Scope is empty, and we give univ 
	// the default scope
	if (command_.leafId2Scope.isEmpty()) {
	    // univ is the only sig and default scope _must_ be >= 0
	    Dbg.chk(SigType.getStringToType().size() == 1 && defaultScope >= 0); 
	    command_.leafId2Scope.put(_moduleInfo.getUniv().getLeafId(),
				      new Integer(defaultScope));
	}

	// handle product signatures
        _handleProductSigs(command_.leafId2Scope, command_.productSigIdsToRels);
	// set intwidth if specified
	command_.intWidth = _getIntWidth(scope);
        // check that subscopes have been set legally
        _checkSubScopes(command_);
    }

    /**
     * this method assumes that id_ is not the LeafId of univ.
     * @return true if SigType associated with id_ is a top-level type
     **/
    private boolean _isTopLevel(LeafId id_) {
	return (_scopedSigsInfo.parentSigId(id_) == _moduleInfo.getUniv().getLeafId());
    }

    /**
     * @return true if the Signature that has SigType type_ is abstract;
     * otherwise returns false
     **/
    private static boolean _isAbstract(String type_) {
	return SigType.getSigTypeForString(type_).getSignature().isAbstract();
    }

    /**
     * @param id_ LeafId of SigType which we are testing for scoped subtypes
     * @param leafId2Scope_ Map of LeafIds to scopes
     * @return true if SigType associated with id_ has a scoped subtype; 
     * otherwise returns false.
     **/
    private boolean _hasScopedSubtype(LeafId id_, Set explicitlyScopedSigs_) {
	
	for (Iterator children = _scopedSigsInfo.childSigIds(id_); children.hasNext(); ) {
	    LeafId child = (LeafId) children.next();
	    if (explicitlyScopedSigs_.contains(child) ||
		_hasScopedSubtype(child, explicitlyScopedSigs_))
		return true;
	}
	return false; 
    }

    
    
    /** @return true if signature sigName_ is static */
    private static boolean _isOneOrLoneSig(String sigName_) {
        SigType sigType = SigType.getSigTypeForString(sigName_);
        if (sigType != null) {
            Multiplicity mult = sigType.getSignature().getMult();
            return mult.equals(Multiplicity.ONE) || mult.equals(Multiplicity.LONE);
        }
        return false;
    }

    /** @return LeafId associated with the given signature name **/
    private LeafId _sigLeafId(String sigName_) {
	return _scopedSigsInfo.getScopedSigId(sigName_);
    }
    
    /**
     * Creates a mapping from leafId to scope in leafId2Scope and returns scope
     **/
    private int _updateLeafId2Scope(Map leafId2Scope, LeafId leafId, int scope) {
	leafId2Scope.put(leafId, new Integer(scope));
	//System.out.println("Assigned scope of " + scope + " to " + _scopedSigsInfo.getScopedSigName(leafId));
	return scope;
    }

    /**
     * This method handles an unscoped type as follows:  
     * if curType_ is a sig with multiplicity one or lone, it gets the scope of 1; 
     * if curType_ an abstract sig with scoped children,
     * its scope becomes the sum of children's scopes; 
     * if curType_ has an abstract parent and all of its siblings
     * are scoped, then curType_ is given the scope of parent minus
     * the sum of the scopes of its siblings;
     * if curType_ is a top-level type and defaultScope_ >= 0,
     * then curType_ gets the default type.  
     * @param curType_ name of the type to be scoped
     * @param leafId2Scope_ Map from LeafIds to Integers representing 
     * the scopes associated with LeafIds
     * @param defaultScope_ the default scope; if defaultScope_ < 0, none is used
     * @return scope for curType_ or -1 if the scope cannot be determined.  
     * If a scope is succesfully determined, this method will add the mapping (
     * LeafId of curType_)->(scope for curType_) to leafId2Scope_.
     **/
    private int _scopeType(String curType_, Map leafId2Scope_, int defaultScope_) {
    
	
	LeafId curId = _sigLeafId(curType_);

	// the scope has already been assigned -- just return it
	if (leafId2Scope_.containsKey(curId)) {
	    return ((Integer) leafId2Scope_.get(curId)).intValue();
	} 
	    
	// sigs with multiplicity one or lone have an implicit scope of 1
	if (_isOneOrLoneSig(curType_)) { 
	    return _updateLeafId2Scope(leafId2Scope_, curId, 1);
	}

	// If we have an unscoped abstract type whose children are all scoped, its
	// scope is taken to be the sum of children's scopes.
	if (_isAbstract(curType_)) {
	    
	    Iterator children = _scopedSigsInfo.childSigIds(curId);

	    // if no children, nothing to do . . .
	    int scopeSum = (children.hasNext() ? 0 : -1);
		
	    while (children.hasNext()) {
		LeafId child = (LeafId) children.next();
		int childScope = _scopeType(_scopedSigsInfo.getScopedSigName(child),
					    leafId2Scope_, defaultScope_);
		if (childScope == -1) {
		    scopeSum = -1;
		    break;
		} else {
		    scopeSum += childScope;
		}
	    }
	    if (scopeSum >= 0)
		return _updateLeafId2Scope(leafId2Scope_, curId, scopeSum);
	    
	}

	// If we have a child of a scoped abstact sig whose sibling are all scoped,
	// then the scope of the child is the scope of the parent minus the sum of the
	// scopes of siblings
	LeafId parentId = _scopedSigsInfo.parentSigId(curId);
	if ((parentId != null) && _isAbstract(_scopedSigsInfo.getScopedSigName(parentId)) &&
	    leafId2Scope_.containsKey(parentId)) {
	    // we temporarily map curId to -1, so that we don't get into an infinite loop
	    // in situations where two unscoped children of a scoped abstract sig are 
	    // recursively calling the method back and forth between each other
	    leafId2Scope_.put(curId, new Integer(-1));
	    int sibScopes = 0;
	    for (Iterator siblings = _scopedSigsInfo.childSigIds(parentId); 
		 siblings.hasNext();) {
		LeafId sibling = (LeafId) siblings.next();
		if (sibling.equals(curId)) { continue; } //
		int sibScope = _scopeType(_scopedSigsInfo.getScopedSigName(sibling),
					  leafId2Scope_, defaultScope_);
		if (sibScope == -1) {
		    sibScopes = -1;
		    break;
		} else {
		    sibScopes += sibScope;
		}
	    }
	    int parentScope = ((Integer)leafId2Scope_.get(parentId)).intValue();
	    if ((sibScopes >= 0) && (parentScope - sibScopes >= 0))
		return _updateLeafId2Scope(leafId2Scope_, curId, parentScope - sibScopes);
	    // remove the temporary mapping to -1
	    leafId2Scope_.remove(curId);
	}
			
	// If curType_ is an unscoped top-level type, we assign
	// default scope to it, if there is one
	if (_isTopLevel(curId) && (defaultScope_ >= 0)) {
	    return _updateLeafId2Scope(leafId2Scope_, curId, defaultScope_);
	} 
		
	return -1;
	    
	
    }

    /**
     * @return an Integer that is the sum of the scopes of all signatures 
     * extending sig_.  The method works as follows:  if a given child of 
     * sig_ has a scope, that scope is added to the sum.  If it doesn't,
     * then we add the sum of the scope of its descendents to the return value.
     **/
    private static int _sumDescendents(Signature sig_, Map leafId2Scope_) {
	int sum = 0;
	for (Iterator childSigs = sig_.getExtByIter(); childSigs.hasNext(); ) {
	    Signature childSig = (Signature) childSigs.next();
	    LeafId childId = childSig.getLeafId();
	    if (leafId2Scope_.containsKey(childId)) {
	        sum += ((Integer) leafId2Scope_.get(childId)).intValue();
	    } else {
		sum += _sumDescendents(childSig, leafId2Scope_);
	    }
	}
	return sum;
    }

    /**
     * @return true if sig_ has children and all of them are scoped; otherwoise
     * returns false.
     **/
    private static boolean _allChildrenScoped(Signature sig_, Map leafId2Scope_) {
	Iterator childSigs = sig_.getExtByIter();
	if (!childSigs.hasNext())
	    return false;

	while (childSigs.hasNext()) {
	    if (!leafId2Scope_.containsKey(((Signature) childSigs.next()).getLeafId()))
		return false;
	}

	return true;
    }

    /**
     * This method makes sure that scope settings for command_ are consistent:
     * sum of children's scopes must not be greater than the parent signature's scope,
     * and, if the parent is abstract and all of its children are scoped, then the
     * sum of the children's scopes must be equal to the scope of the parent.
     */
    private void _checkSubScopes(Command command_) {

	for (Iterator sigTypeIter = SigType.getStringToType().values().iterator();
             sigTypeIter.hasNext(); ) {

            Signature sig = ((SigType)sigTypeIter.next()).getSignature();
	    LeafId sigId = sig.getLeafId();


	    // see if scope has been set for sig; we only care that the scoped sigs have
	    // been assigned correct scopes.  Any unscoped signatures *must* be transitive
	    // subtypes of scoped top-level signatures at this point.
	    	    
	    if (!command_.leafId2Scope.containsKey(sigId)) { continue; }

	    // add up scopes of all sigs extending sig
	    int childSigScopes = _sumDescendents(sig, command_.leafId2Scope);
	    
	    // make sure childSigScopes is not greater than scope of sig
	    int sigScope = ((Integer)command_.leafId2Scope.get(sigId)).intValue();

	    if (sigScope < childSigScopes) {
		Dbg.user(new Msg("the sum of scopes " + childSigScopes + 
				 " of signatures extending " + sig.getTypedName() +
				 " must not be greater than the scope " + 
				 sigScope + " of " + sig.getTypedName(),
				 command_));
		continue;
	    }

	    
            // if sig is abstract and all of its children are scoped, then its scope
	    // must be equal to the sum of the children's scopes.
	    if (sig.isAbstract() && _allChildrenScoped(sig, command_.leafId2Scope) &&
		(sigScope != childSigScopes)) {
		                     
		Dbg.user(new Msg("the sum of scopes " + childSigScopes + 
				 " of signatures extending " + sig.getTypedName() +
				 " must be the same as the scope " + sigScope + 
				 " of abstract signature " + sig.getTypedName(),
				 command_));
	    }
	}
    }
    
    /**
     * add specified type scopes to a mapping, checking each to see if it is valid
     */
    private boolean _addTypeScopesToMapping(Scope scope_, Map leafId2Scope_) {
	
	for (Iterator scopeIter = scope_.getTypeScopes().getTypeScopeIter();
	     scopeIter.hasNext();) {
            TypeScope curTypeScope = (TypeScope)scopeIter.next();
            SigExpr curSigExpr = curTypeScope.getSigExpr();
            //Dbg.info(curSigExpr.toString());
            // skip spec of "int"

            if (curSigExpr.nodeString().equals("int")) { continue; }
            String curType = _fullyQualifiedTypeString(curSigExpr);
	    	    
            if (curType == null) return false;
            // make sure String corresponds to a scoped sig or Int
            LeafId typeId = _sigLeafId(curType);
	    //System.out.println("in addType... typeId " + typeId);
            if (typeId == null) {
		Dbg.user(new Msg("scope specified for invalid type", curSigExpr));
                return false;
            }
            // make sure type has not already been mapped
            if (leafId2Scope_.containsKey(typeId)) {
                Dbg.user(new Msg("duplicate specification of scope for type", curSigExpr));
                return false;
            }
            // make sure current type is not a product sig
            if (_isProductSig(curType)) {
                Dbg.user(new Msg("scope specified for product signature", curSigExpr));
                return false;
            }
	    // make sure that a one or lone sig is assigned the scope of 1
	    if (_isOneOrLoneSig(curType) && (curTypeScope.getBound() != 1)) {
		Dbg.user(new Msg("scope of " + curType + " must be 1",
				 curSigExpr));
		return false;
	    }
            // add mapping
            leafId2Scope_.put(_sigLeafId(curType), new Integer(curTypeScope.getBound()));
            
        }
        // scopes had no errors
        return true;
    }

    /**
     * create a String with the fully qualified names of all signatures mentioned in a SigExpr,
     * for use in matching to a type
     */
    private String _fullyQualifiedTypeString(SigExpr sigExpr_) {
        
	QualifiedName baseName = sigExpr_.getSig();
	        
	Signature sigPara = _moduleInfo.getSignature(baseName, "set scope");
	
	if (sigPara == null) {
	    return null;
	} else {
	    baseName = sigPara.getName();
	}
        
	return baseName.nodeString();
    }
    
    private int _getIntWidth(Scope scope_) {
	
        int intWidth = -1;
	for (Iterator scopeIter = scope_.getTypeScopes().getTypeScopeIter(); scopeIter.hasNext();) {
            TypeScope curScope = (TypeScope)scopeIter.next();
            if (curScope.getSigExpr().nodeString().equals("int")) {
                if (intWidth != -1) {
                    Dbg.user(new Msg("duplicate declaration of int width", curScope));
                    return -1;
                } else {
                    intWidth = curScope.getBound();
                }
            }
        }
        return intWidth;
    }


    /**
       Set the scopes of product sigs.  Scope is set to the product of the
       scope required to enumerate all possible values of each field.  If a
       field relation has arity 2, and its right type has scope k, it
       contributes a factor k to the scope if it has scalar multiplicity,
       k + 1 for option multiplicity, and 2^k for set multiplicity.  For relations
       (ie. field relations with arity >= 3),
       we ignore multiplicities for now, and just add 2^k for each basic type in the
       rhs of the declaration of the relation. 
     */
    private void _handleProductSigs(Map leafId2Scope_, Map productSigIdsToRels_) {
        for (Iterator typeIter = SigType.getSigTypeStrings().iterator(); 
	     typeIter.hasNext();) {
            String curType = (String)typeIter.next();
	    Signature curSig = SigType.getSigTypeForString(curType).getSignature();
            if (curSig.isProduct()) {
                int productScope = 1;
                // iterate through decls, multiplying product scope
                // by factor for each field

                // keep a map from relations declared in the signature to their
                // multiplicity exprs
                Map relIdToMultExpr = new HashMap();
                for (Iterator declIter = curSig.getDecls().getDeclIter(); declIter.hasNext(); ) {
                    productScope *= _productDeclScope(curSig, (Decl)declIter.next(), leafId2Scope_, relIdToMultExpr);
                }
		leafId2Scope_.put(_sigLeafId(curType),new Integer(productScope));
                LeafId sigId = curSig.getLeafId();
                productSigIdsToRels_.put(sigId, relIdToMultExpr);
            }
        }
    }

    private int _productDeclScope(Signature sig_, Decl decl_, Map leafId2Scope_,
                                  Map relIdToMultExpr_) {
        MultiplicityExpr multExpr = decl_.getExpr();
        // first, add appropriate entries to relIdToMultExpr_ map
        for (Iterator varIter = decl_.getVariables().getVariableIter(); varIter.hasNext(); ) {
            Variable var = (Variable)varIter.next();
            LeafId relId = sig_.getFieldLeafId(var.nodeString());
            relIdToMultExpr_.put(relId, multExpr);
        }
        UnionType type = multExpr.getType();
        int numVars = decl_.getVariables().numChildren();
        if (multExpr instanceof SetMultExpr
            && type.arity() == 1) {
            return _setMultDeclScope(numVars,
                                     (SetMultExpr)multExpr,
                                     type, leafId2Scope_);
        } else {
            return _arrowMultDeclScope(numVars,
                                       type, leafId2Scope_);
        }
    }

    private int _setMultDeclScope(int numVars_,
                                  SetMultExpr sMultExpr_,
                                  UnionType type_,
                                  Map leafId2Scope_) {
        Multiplicity mult = sMultExpr_.getMult();
        int fieldScope = ((Integer)leafId2Scope_.get(((RelationType)type_.getTypeIter().next()).getBasicTypeAt(0).toString())).intValue();
        if (mult.equals(Multiplicity.LONE)) {
            fieldScope++;
        } else if (mult.equals(Multiplicity.SET)) {
            fieldScope = 1 << fieldScope;
        }
        return fieldScope * numVars_;
    }

    private int _arrowMultDeclScope(int numVars_,
                                    UnionType type_,
                                    Map leafId2Scope_) {
        int fieldScope = 1;
        for (int i = 0; i < type_.arity(); i++) {
            fieldScope *= 1 << ((Integer)leafId2Scope_.get(((RelationType)type_.getTypeIter().next()).getBasicTypeAt(i).toString())).intValue();
        }
        return fieldScope * numVars_;
    }

     private static boolean _isProductSig(String sigName_) {
        SigType sigType = SigType.getSigTypeForString(sigName_);
        if (sigType != null) {
            Signature sig = sigType.getSignature();
            return sig.isProduct();
        }
        return false;
    }

        
}
        
            

